package ch.epfl.lara.matcheck.ast.parser;

import scala.util.parsing.combinator.syntactical.StdTokenParsers

trait FormulaParser extends SyntaxParser with ParsingHelper  { self: SyntaxParser => 

  getLexical.reserved ++= List ("\\subseteq","\\Un","\\Int","\\in","\\forall","empty")

  getLexical.delimiters ++= List("<-->","-->")
  
  
  def DomainFormula: Parser[Formula] = positioned(
        Domain ~ opt( (("&" ^^^ And) | ("|" ^^^ Or) ) ~ DomainFormula) 
               ^^ { case lhs ~ oprhs => oprhs match {
                      case None => lhs
                      case Some(~(op,rhs)) => op(lhs,rhs)
                  }}
      | failure("illegal start of formula definition")
  )
  
  /**
   * F ::=   F0 { ( "&" | "|" ) F }
   *	   | "~" F
   */
  def F: Parser[Formula] = positioned(    
      //F0 ~ rep(( ( "&" ^^ And _) | ( "|" ^^ Or _) ) ~ F)     ^^ flatten2(mkBinaryRelation[Formula] _)
      F0 ~ opt((    "&"    ^^ (_ =>"&") 
             |  "|"    ^^ (_ => "|") 
             |  "<-->" ^^ (_ =>"<-->")
             |  "-->"  ^^ (_ => "-->")
           ) ~ F)     ^^ { case lhs ~ op_rhs => op_rhs match {
                                                     case None => lhs 
                                                     case Some(~(op,rhs)) => 
                                                       op match {
                                                         case "&"    => And(lhs,rhs)
                                                         case "|"    => Or(lhs,rhs)
                                                         case "<-->" => And(Or(Neg(lhs),rhs),Or(lhs,Neg(rhs)))
                                                         case "-->"  => Or(Neg(lhs),rhs)
                                }}}
           
    | "~" ~> F                                    ^^ {case f => Neg(f) }
    | failure("illegal start of formula definition")
  )

  
  /**
   * F0 ::=   A
   *	    | "(" F ")"
   */
  def F0: Parser[Formula] = positioned(
      "(" ~> F <~ ")"
    | A
    | failure("illegal start of formula definition")
  )
  
  
  /**
   * A ::=   "\forall" x "." F 
   *       | M "\subseteq" M 
   *	   | E "\in" M 
   *	   | Cop 
   *	   | "true" 
   *	   | "false" 
   */
  def A: Parser[Atom] = positioned(
      "\\forall" ~> ident ~ "." ~ F               ^^ { case x ~ "." ~ f => Forall(x,f) }
    | CA
    | failure("illegal start of predicate formula definition")
  )
  
  def CA: Parser[Atom] = positioned(
       Domain
    |  Cop
    | failure("illegal start of predicate formula definition")  
  )
  
  def Domain: Parser[Atom] = positioned(
        M ~ (  "\\subseteq" ^^^ SubsetEq 
          | "=" ^^^ EqSet) ~ M                   ^^ { case lhs ~ op ~ rhs => op(lhs,rhs)}
      | failure("illegal start of predicate formula definition")
  )
  
   /**
   * Cop ::= E ( "<" | "<=" | ">" | ">=" | "==" | "!=" ) E
   */
  def Cop: Parser[Atom] = positioned(
        E ~ opt( ( ((  "<"    ^^^ createCmpExpr(false)(Less) _
                 | "<="    ^^^ createCmpExpr(false)(LessEq) _
                 | ">"     ^^^ createCmpExpr(true)(Less) _
                 | ">="    ^^^ createCmpExpr(true)(LessEq) _
                 | "=="    ^^^ createCmpExpr(false)(Eq) _
                 | "!="   ^^^ createCmpExpr(false)(NotEq) _
               ) ~ E) ^^ { case op ~ rhs => partialCmp(op,rhs) })
             | ( ( "\\in" ^^^ In) ~ M) ^^ { case op ~ rhs => partialSetInclusion(op,rhs) })
          ^^ { case lhs ~ op => op match {case Some(op) => op(lhs) case None => lhs}}
      | failure("illegal start of boolean expression")
  )   
  
  def partialCmp(op: (E,E) => Atom, rhs: E) = { lhs: E => op(lhs,rhs) } 
  
  def partialSetInclusion(op: (E,SetExpr) => Atom, rhs: SetExpr) = { lhs: E => op(lhs,rhs) }
  
  /**
   * M ::= M0 { ("\\Un" | "\\Int") M0 }
   */
  def M: Parser[SetExpr] = positioned(
      "(" ~> M <~")"
    | M0  ~ rep( (   ( "\\Un"  ^^^ Union)  
                   | ("\\Int" ^^^ Intersection) 
                 ) ~ M )                ^^ { case first ~ rest => mkBinaryRelation[SetExpr](first,rest) }
    | failure("illegal start of set domain definition")
  )

  
  /**
   * M0 ::=   ident 
   *            | "empty" 
   */
  def M0: Parser[SetExpr] = positioned(
      ident                                      ^^ { case name => Set(name) } 
    | "empty"                                    ^^^ EmptySet
    | failure("illegal start of set domain definition")
  )
  
  
 
  
  /**
   * E ::=   stringLit
   *	   | "true"
   *	   | "false" 
   * 	   | T 
   *	   | T0
   */
  def E: Parser[E] = positioned(
      stringLit                                  ^^ {case name => StringLit0(name) } 
    | "true"                                     ^^^ Tru
    | "false"                                    ^^^ Flse
    | T0
    | failure("illegal start of elem definition")
  )
   
  
  /**
   * T ::= ident [ "(" { T } ")" | "." T ] 
   */  
  def T: Parser[Term] = positioned(
      ident ~ opt("(" ~> rep(T) <~ ")" | "." ~> T)       ^^ { case name ~ arg => arg match {
                                                                         case None    => Element(name)
                                                                         case Some(t: CodeTerm) => Deref(Element(name),t)
                                                                         case Some(a: List[x]) => Function(name,a.asInstanceOf[List[Term]])
                                                                         
                                                       }}         
  
    | Numeric
    | failure("illegal start of term formula definition")
  )

  
  
  /**
   * T0 ::= TPrecedence { ( "+" | "-" ) T0 }
   */
  def T0: Parser[Term] = positioned(
      TPrecedence ~ rep ( ( "+" ^^^ Plus 
                           |"-" ^^^ Minus
               ) ~ T0)    ^^ { case first ~rest => mkBinaryRelation[Term](first,rest) }
    | failure("illegal start of arithmetic expression")   
  )
   
  
  /**
   * TPrecedence ::= T1 { ( "%" | "/" | "*" ) TPrecedence }
   */
  def TPrecedence: Parser[Term] = positioned(
      T ~ rep( (   "%" ^^^ Mod  
                  | "/" ^^^ Div 
                  | "*" ^^^ Prod 
                )  ~ TPrecedence )        ^^ { case first ~ rest => mkBinaryRelation[Term](first,rest) }         
    | failure("illegal start of arithmetic expression")
  )
  
  /**
   * Number ::= [ "-" ] numericLit
   */
  def Numeric: Parser[Term] = positioned(
      opt("-") ~ numericLit ^^ {case sign ~ number => sign match {
                                                            case Some("-") => Const(-number.toInt)
                                                            case _ => Const(number.toInt) 
                                       }}
     | failure("illegal start of simple term")
  )
  
  
 
}